| Definitions |  x:A. B(x), P   Q, interfaceGlue(A; I; l; tg; nmr), t  T, Realizer, if b then t else f fi ,   b, (x,yL. P(x;y)), xL. P(x),   x. t(x), ||as||, l[i], Y, P  Q, A, SQType(T), {T},  , hd(l), nth_tl(n;as), i  z j, tl(l), i <z j, tt, ff,  , A B, False, P & Q, P  Q, P Q, {i..j }, i j < k, (x l),  x:A. B(x), A c B, S  T, ma-interface-ds(I;i), t.2, a:A fp B(a), Knd, t.1, True, ma-interface-conds(I;i), f(x), Top,  b, es-in-port-conds(A;l;tg), x : v, Normal(ds), x,y. t(x;y), x(s), Dec(P), Namer(n;Id_list),  , Unit, MaInterface(T), ma-interface-locs(I), rcv(l,tg), isrcv(k), lnk(k), isl(x), outl(x), gluable2(A;I;l;tg), (xL.P(x)), x dom(f), Normal(A,I), x(s1,s2),  , ma-interface-domb(I;i;k), ma-interface-dom(I;i), ma-interface-info(I;i;k), ma-interface-valtype(I;i;k) |
| Lemmas | interfaceGlue helper, interfaceGlue helper2, R-feasible-Rlist, Rall wf, decidable int equal, int seg wf, R-compat-Rall2, member filter, l member wf, R-feasible-Rall, decidable equal Id, R-compat wf, R-Feasible wf, unit wf, Id wf, rationals wf, Knd wf, fpf wf, decl-state wf, decl-type wf, IdLnk wf, finite-prob-space wf, bool wf, gluable2 wf, gluable wf, ma-interface-normal wf, Namer wf, le wf, append wf, lname wf, ma-interface-tags wf, ma-interface wf, assert wf, bnot wf, eq id wf, lsrc wf, not wf, and functionality wrt iff, member-remove-repeats, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, mk lnk wf, ma-interface-ds wf, triggersGlue-compatible, eqtt to assert, assert-ma-interface-loc, eqff to assert, nat wf, length wf1, select wf, ma-interface-dom wf, hasloc wf, fpf-ap wf, member-fpf-domain, fpf-trivial-subtype-top, top wf, id-deq wf, subtype rel product, subtype rel list, subtype rel set, subtype rel function, subtype-set-hasloc, interfaceGlue helper0, fpf-join-list wf, mapl wf, assert-ma-interface-domb, ma-interface-dom-hasloc, ma-interface-domb wf, interfaceGlue helper0.5, assert-hasloc, Id sq, fpf-domain wf, ma-interface-conds wf, es-in-port-conds wf, fpf-join-list-ap2, Kind-deq wf, rcv wf, member-mapl, bool sq, fpf-dom wf, assert-deq-member, member append, ma-interface-locs wf, ma-interface-tags-property2, isrcv wf, pi1 wf, triggersGlue feasible2, triggersGlue-compatible2, triggersGlue feasible, fpf-all-empty, interfaceGlue helper0.6 |